the_es:ES, l:IdLnk, e':E, m:(Msg on l).
(m  msgs(l;before(e')))  (e:E. (((e <loc e') & (haslnk(l;e))) c (m = emsg(e)))) 

latex

Definitions	x:A. B(x), P  Q, msgs(l;before(e')), x:A. B(x), A c B, P & Q, P  Q, , P  Q, t  T, x. t(x), (x  l), S  T, A  B, A, False, T, True, x(s), , SqStable(P)
Lemmas	all functionality wrt iff, event system wf, IdLnk wf, es-E wf, es-Msgl wf, iff wf, l member wf, map wf, assert wf, es-haslnk wf, es-msg wf2, es-rcvs wf, es-locl wf, iff functionality wrt iff, member map, length wf1, select wf, member-es-rcvs, sq stable from decidable, decidable assert